0.00/0.36	NO
0.00/0.37	
0.00/0.37	Problem:
0.00/0.37	 f x x -> a
0.00/0.37	 f x (s x) -> b
0.00/0.37	 mu (\x. Z x) -> Z (mu (\x. Z x))
0.00/0.37	
0.00/0.37	Proof:
0.00/0.37	 Higher-Order Church Rosser Processor:
0.00/0.37	  f x x -> a
0.00/0.37	  f x (s x) -> b
0.00/0.37	  mu (\x. Z x) -> Z (mu (\x. Z x))
0.00/0.37	  critical peaks: 0
0.00/0.37	   
0.00/0.37	   
0.00/0.37	   Redundant Rules Transformation for Pattern Rewrite Systems:
0.00/0.37	    f x x -> a
0.00/0.37	    f x (s x) -> b
0.00/0.37	    mu (\x. Z x) -> Z (mu (\x. Z x))
0.00/0.37	    mu (\x. 70 x) -> 70 (70 (mu (\x. 70 x)))
0.00/0.37	    f (mu (\x. s x)) (mu (\x. s x)) -> b
0.00/0.37	    Higher-Order Church Rosser Processor:
0.00/0.37	     f x x -> a
0.00/0.37	     f x (s x) -> b
0.00/0.37	     mu (\x. Z x) -> Z (mu (\x. Z x))
0.00/0.37	     mu (\x. 70 x) -> 70 (70 (mu (\x. 70 x)))
0.00/0.37	     f (mu (\x. s x)) (mu (\x. s x)) -> b
0.00/0.37	     critical peaks: 8
0.00/0.37	      a <-[]-> b
0.00/0.37	      105 (mu (\x. 105 x)) <-[]-> 105 (105 (mu (\x. 105 x)))
0.00/0.37	      f (s (mu (\x. s x))) (mu (\x. s x)) <-[0,1]-> b
0.00/0.37	      f (mu (\x. s x)) (s (mu (\x. s x))) <-[1]-> b
0.00/0.37	      115 (115 (mu (\x. 115 x))) <-[]-> 115 (mu (\x. 115 x))
0.00/0.37	      f (s (s (mu (\x. s x)))) (mu (\x. s x)) <-[0,1]-> b
0.00/0.37	      f (mu (\x. s x)) (s (s (mu (\x. s x)))) <-[1]-> b
0.00/0.37	      b <-[]-> a
0.00/0.37	      
0.00/0.37	      Higher-Order Nonconfluence Processor:
0.00/0.37	       non-joinable conversion:
0.00/0.37	       a *<- a <- f (mu (\x. s x)) (mu (\x. s x)) -> b ->* b
0.00/0.37	       Qed
0.00/0.37	 
0.00/0.37	EOF